(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_LRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 3))
(let ((e4 (- v1 v2)))
(let ((e5 (/ e3 (- e3))))
(let ((e6 (- v0 v1)))
(let ((e7 (>= v0 v2)))
(let ((e8 (= e4 v0)))
(let ((e9 (= e5 e5)))
(let ((e10 (<= e6 e5)))
(let ((e11 (>= v1 v0)))
(let ((e12 (distinct v0 v2)))
(let ((e13 (distinct e4 v1)))
(let ((e14 (>= v2 e6)))
(let ((e15 (< v0 v1)))
(let ((e16 (>= v2 e5)))
(let ((e17 (= e16 e8)))
(let ((e18 (xor e10 e14)))
(let ((e19 (and e12 e12)))
(let ((e20 (=> e9 e18)))
(let ((e21 (xor e11 e15)))
(let ((e22 (= e7 e21)))
(let ((e23 (= e22 e22)))
(let ((e24 (and e19 e23)))
(let ((e25 (not e20)))
(let ((e26 (=> e25 e13)))
(let ((e27 (= e26 e26)))
(let ((e28 (not e27)))
(let ((e29 (or e24 e17)))
(let ((e30 (= e28 e29)))
e30
)))))))))))))))))))))))))))))

;; CHECK: (assert (= v0 (/ 86 (- 58))))
;; CHECK: (assert (= v1 (/ (- 88) (- 29))))
;; CHECK: (check-sat)
(check-sat-assuming-model (v0 v1) ((/ 86 (- 58)) (/ (- 88) (- 29))))
